$\forall$$T$:Type, $c$:$T$, $i$:Id. constR\{x:ut2\}($T$; $c$; $i$) $\in$ Realizer